perm filename RUNT[P,JRA]1 blob
sn#059063 filedate 1973-09-05 generic text, type T, neo UTF8
00050 (SETQ NEGSGN @¬)
00100
00150
00200
00250 (DEFPROP THSET
00300 (LAMBDA(A B)
00350 (EVAL(LIST @THSETQ A(LIST @QUOTE B)T T)))
00400 EXPR)
00450
00500 (DEFPROP THVSET
00550 (LAMBDA(A B)
00600 (EVAL(LIST @THVSETQ A(LIST @QUOTE B))))
00650 EXPR)
00670
00672
00674 (DEFPROP GETNUMARG
00676 (LAMBDA(X)
00678 (COND((EQ(CAR X)@#)(CAADDR X))
00680 (T(CAR X))) )
00682 EXPR)
00684
00686
00700
00702
00704 (DEFPROP NEWVAR
00708 (LAMBDA(X)
00712 (PROG (XT)
00713 (SETQ XT X)
00714 NE1 (THSET (CAR XT)(READLIST(APPEND(LIST @X)(EXPLODE(THSETQ(THV XN)(ADD1(THV XN)))))))
00717 (THVAL(LIST @THASSERT(LIST @ISVAR (CAR XT)))THALIST)
00719 (SETQ XT(CDR XT))
00721 (COND(XT(GO NE1)))
00722 (RETURN T) ))
00724 FEXPR)
00728
00732
00734 (DEFPROP GZ
00736 (LAMBDA(X)
00738 (AND(NOT(MINUSP (CAR X)))(NOT(ZEROP (CAR X)))) )
00740 EXPR)
00742
00744 (DEFPROP GT
00746 (LAMBDA(X Y)
00748 (*GREAT (CAR X)(CAR Y)) )
00750 EXPR)
00752
00754
00756 (DEFPROP SUB2
00758 (LAMBDA(X)
00760 (SUB1(SUB1 X)) )
00762 EXPR)
00764
00766
00800
00850 (SETQ ADVBRL @((FOR . AD1)(DELETE . AD2)(ADD . AD3)(ALTER . AD4)(ASSUME . AD5)
00900 (RESTRICT . AD6)(ADVICE . AD7)(STATUS . AD8)))
00950
01000
01050 (DEFPROP ADVICESYS
01100 (LAMBDA NIL
01150 (PROG(ADV ALR NA OPT LL VN)
01200 (TERPRI)(PRINT @*********___ENTERING__ADVICE__SYSTEM___*********)(TERPRI)
01250 (SETQ SSW T)
01300 AD01 (SETQ OPT NIL)
01350 (PRINT(READLIST(APPEND @(#)(EXPLODE(ADD1 AN)))))
01400 (SETQ ADV(READ))
01450 (COND((NULL ADV) (SETQ SSW NIL) (RETURN NIL)))
01500 (COND((EQ ADV T)(SETQ SSW NIL) (RETURN T)))
01550 (SETQ AN(ADD1 AN))
01600 (SETQ ADV(LIST ADV AN))
01650 (SETQ NA(ASSOC(CAR ADV)ADVBRL))
01700 (COND(NA(GO(CDR NA)))
01750 (T(SETQ AN(SUB1 AN))(PRINT @NONESENSE!!)(GO AD01)))
01800 AD1 (SETQ ADV(CONS(READ)ADV))
01850 (SETQ NA(CAR ADV))
01900 (SETQ ADV(CONS(READ)ADV))
01950 (COND((EQ @FIRST(CAR ADV))(SETQ OPT T)
02000 (SETQ ADV(CONS(READ)ADV)) ))
02050 (SETQ ADV(CONS(CONS(READ)(READ))ADV))
02100 (SETQ AL(CONS(REVERSE ADV)AL))
02150 (COND((NULL OPT)(RPLACD(FBODY(GET NA @THEOREM))
02200 (LIST(LIST @THOR(CONS @THAND(CDR(FBODY(GET NA @THEOREM))))
02250 (LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))))))
02300
02350 (T(RPLACD(FBODY(GET NA @THEOREM))
02400 (CONS(LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))
02450 (CDR(FBODY(GET NA @THEOREM)))))))
02500 (PRINT @IS_RULE_DEFINED_FOR_GIVEN_ADVICE?*)
02550 (COND((READ)(GO AD01)))
02600 AD02 (PRINT @DEFINITION_FILENAME_)(PRINC @(ENCLOSE IN PARENS PLEASE))(PRINC @*)
02650 (SETQ LL(READ))
02660 (COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(SETQ FILENAME(CAR LL))(GO AD002)))
02700 (COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
02750 (COMP LL)
02755 AD002 (SETQ VN(THV ZN))
02760 (EVAL(LIST @DSKIN FILENAME))
02770 (COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
02773 (THSETQ(THV ZN)(PLUS VN 10))
02776 (THSETQ(THV YN)(PLUS VN 10))
02779 (THSETQ(THV XN)(PLUS VN 10))
02800 (GO AD01)
02850 AD2 (SETQ NA(READ))
02900 (COND((GET NA @THEOREM)(THVAL(LIST @THERASE NA)THALIST))
02950 ((EQ @#(CAR(EXPLODE NA)))(DELAD NA)(GO AD01))
03000 ((EQ NEGSGN(CAR(EXPLODE NA)))
03050 (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
03100 (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
03150 (SETQ NA(CONS NA(APPEND(READ)@(R)))))
03200 (T(SETQ NA(CONS NA(READ)))))
03250 (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))
03300 (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
03350 (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
03400 (T(SETQ NA(CONS NA(READ)))))
03450 (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))))
03500 (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
03550 (T(SETQ NA(CONS NA(READ)))))
03600 (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST)))) )
03650
03700 (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
03750 (GO AD01)
03800 AD3 (SETQ NA(READ))
03850 (COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
03900 (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
03950 (COND((EQ NEGSGN(CAR(EXPLODE NA)))
04000 (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
04050 (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
04100 (SETQ NA(CONS NA(APPEND(READ)@(R)))))
04150 (T(SETQ NA(CONS NA(READ)))))
04200 (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))
04250 (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
04300 (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
04350 (T(SETQ NA(CONS NA(READ)))))
04400 (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
04450 (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
04500 (T(SETQ NA(CONS NA(READ)))))
04550 (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST)))) )
04600 (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
04650 (GO AD01)
04700 AD4 (SETQ NA(READ))
04750 (COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)
04800 (SETQ AN(SUB1 AN))(GO AD01)))
04850 (SETQ AL(CONS(REVERSE(CONS(GET NA @THEOREM)(CONS NA ADV)))AL))
04900 (THVAL @(THERASE(THEV NA))THALIST)
04950 (REMPROP NA @THEOREM)
05000 (GO AD02)
05050 AD5 (SETQ NA(READ))
05100 (COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
05150 (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
05200 (COND((EQ NEGSGN(CAR(EXPLODE NA)))
05250 (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
05300 (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
05350 (SETQ NA(CONS NA(APPEND(READ)@(R)))))
05400 (T(SETQ NA(CONS NA(READ))))) )
05450 (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
05500 (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
05550 (T(SETQ NA(CONS NA(READ)))))
05600 (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
05650 (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
05700 (T(SETQ NA(CONS NA(READ))))) ) )
05750 (SETQ OPT(READLIST(APPEND @(T)(EXPLODE(CAR NA)))))
05800 (PUTPROP OPT(LIST @THCONSE(PTHV(CDR NA))(CONS(CAR NA)(CDR NA))
05850 (LIST @THSETQ @(THV ASSL)(LIST @CONS NA @(THV ASSL))))
05900 @THEOREM)
05950 (THASSERT(THEV OPT))
06000 (SETQ AL(CONS(REVERSE(CONS OPT ADV))AL))
06050 (GO AD01)
06100 AD6 (SETQ ADV(CONS(READ)ADV))
06150 (SETQ NA(CAR ADV))
06200 (COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)(SETQ AN(SUB1 AN))(GO AD01)))
06250 (SETQ OPT(READ))
06300 (SETQ ADV(CONS OPT ADV))
06350 (SETQ ADV(CONS(READ)ADV))
06400 (COND((EQ OPT @TO)(SET(READLIST(APPEND @(R T)(EXPLODE NA)))
06450 (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R T)(EXPLODE NA)))))))
06500 ((EQ OPT @FROM)(SET(READLIST(APPEND @(R F)(EXPLODE NA)))
06550 (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R F)(EXPLODE NA)))))))
06600 (T(PRINT OPT)(PRINC @_IS_NOT_A_VALID_OPTION)(SETQ AN(SUB1 AN))(GO AD01)))
06650 (SETQ AL(CONS(REVERSE ADV)AL))
06700 (GO AD01)
06750 AD7 (SETQ AN(SUB1 AN))
06800 (TERPRI)(TERPRI)
06850 (COND((NULL AL)(PRINT @NO_ADVICE_GIVEN_THIS_SESSION)(GO AD01)))
06900 (PRINT @**_ADVICE_GIVEN_DURING_THIS_SESSION_**)
06950 (TERPRI)
07000 (SETQ ALR(REVERSE AL))
07050 AD03 (COND((NULL ALR)(GO AD01)))
07100 (COND((EQ @ALTER(CADAR ALR))(GO AD05)))
07150 (PRINT(CAR ALR))
07200 (SETQ ALR(CDR ALR)) (GO AD03)
07250 AD05 (PRINT(LIST(CAAR ALR)(CADAR ALR)(CADDAR ALR)))
07300 (PRINT @DO_YOU_WANT_TO_SEE_PREVIOUS_VERSION?*)
07350 (COND((READ)(SPRINT(CADR(CDDAR ALR))2 2)))
07400 (PRINT @DO_YOU_WANT_TO_SEE_THE_PRESENT_VERSION?*)
07450 (COND((READ)(SPRINT(GET(CADDAR ALR)@THEOREM)2 2)))
07500 (SETQ ALR(CDR ALR))
07550 (GO AD03)
07600 AD8 (SETQ AN(SUB1 AN))
07650 (TERPRI)(TERPRI)
07700 (PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
07750 (PRINT @___)(PRTRULES CT )
07800 (TERPRI)
07850 (PRINT @CURRENT_PLAN:)
07900 (TSLPLAN(REVERSE(EVAL(CAR(THV ANS)))))
07950 (TERPRI)
08000 (PRINT @RULES_AND_GOALS_IN_LONGEST_PATH_OBTAINED_THUS_FAR:)
08050 (PRINT @___)(PRTRULES LCT)
08100 (TERPRI)
08150 (PRINT @LONGEST_PLAN:)
08200 (TSLPLAN LGANS)
08250 (TERPRI)
08300 (GO AD01) ))
08350 EXPR)
08400
08450
08500
08550
08600
08650
08700
08750 (DEFPROP PRTRULES
08800 (LAMBDA(X)
08850 (PROG(TEM)
08900 (COND((NULL X)(RETURN NIL)))
08950 (SETQ TEM(REVERSE X))
09000 PRT2 (PRINC(CAAR TEM))
09050 (SETQ TEM(CDR TEM))
09100 (COND(TEM(GO PRT2))) ))
09150 EXPR)
09200
09250
09300 (DEFPROP PTHV
09350 (LAMBDA(ARL)
09400 (COND((NULL ARL)NIL)
09450 ((ATOM(CAR ARL))(PTHV(CDR ARL)))
09500 (T(APPEND(LIST(CADAR ARL))(PTHV(CDR ARL))))))
09550 EXPR)
09600
09650
09700
09750 (DEFPROP TREEPATH
09800 (LAMBDA(OP)
09850 (PROG NIL
09900 (SETQ CT (CONS(LIST(CAR OP))CT ))
09950 (THSETQ (THV CGL)(THVARSUBST(CADR OP)))
10000 (COND((*GREAT(LENGTH CT )(LENGTH LCT))
10050 (SETQ LCT CT )))
10100 (RETURN T)))
10150 FEXPR)
10200
10250
10300 (DEFPROP TRACEINFO1
10350 (LAMBDA NIL
10400 (PROG NIL
10450 (PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
10500 (PRINT @___)
10550 (PRTRULES CT )
10600 (TERPRI)
10650 (RETURN T) ))
10700 EXPR)
10750
10800
10850
10900 (DEFPROP TRACEINFO2
10950 (LAMBDA (OP)
11000 (PROG NIL
11050 (PRINT(CAR OP))(PRINC @_IS_FAILING!!!!)
11100 (COND((NOT(ATOM(CAAR CT )))
11150 (PRINT @___)(PRINC(CADAAR CT ))
11200 (PRINC @_WAS_THE_LOSER) ))
11250 (TERPRI)
11300 (COND((AND(TTYIN)(ADVICESYS))(RETURN T)))
11350 (SETQ CT(CDR CT))
11400 (RETURN NIL) ))
11450 FEXPR)
11500
11550
11600
11650 (DEFPROP DELAD1
11700 (LAMBDA(NU L)
11800 (COND((NULL L)NIL)
11850 ((EQ NU(CAAR L))(DELAD1 NU(CDR L)))
11900 (T(CONS(CAR L)(DELAD1 NU(CDR L))))))
12000 EXPR)
12050
12100
12150 (DEFPROP DELRL
12200 (LAMBDA(RL EL)
12250 (PROG NIL (PRINT RL)(PRINT EL)
12300 (COND((NULL RL)NIL)
12350 ((MEMQ(CAR RL)EL)(DELRL(CDR RL)EL))
12400 (T(CONS(CAR RL)(DELRL(CDR RL)EL)))))
12450 )
12500 EXPR)
12550
12600
12650 (DEFPROP DELAD
12700 (LAMBDA(NUM)
12750 (PROG(AD TE)
12800 (PRINT @L1825)(PRINT NUM)
12850 (SETQ AN(SUB1 AN))
12900 (SETQ AD(ASSOC(READLIST(CDR(EXPLODE NUM)))AL))
12950 (COND((NULL AD)(PRINT @NO_SUCH_ADVICE_GIVEN)(RETURN T)))
13000 (SETQ AL(DELAD1(READLIST(CDR(EXPLODE NUM)))AL))
13050 (PRINT @L1841)(PRINT AD)(PRINT AL)
13100 (SETQ AD(CDR AD))
13150 (GO(CDR(ASSOC(CAR AD)@((FOR . DE1)(DELETE . DE2)(ADD . DE3)(ALTER . DE4)(ASSUME . DE5)(RESTRICT . DE6)))))
13200 DE1 (SETQ AD(CDR AD))
13250 (COND((EQ @FIRST(CADR AD))
13300 (RPLACD(FBODY(GET(CAR AD)@THEOREM))
13350 (CDDR(FBODY(GET(CAR AD)@THEOREM)))))
13400 (T(RPLACD(FBODY(GET(CAR AD)@THEOREM))
13450 (CDADDR(FBODY(GET(CAR AD)@THEOREM))))))
13500 (RETURN T)
13550 DE2 (THVAL @(THASSERT(THEV(CADR AD)))THALIST)
13600 (RETURN T)
13650 DE3 (THVAL @(THERASE(THEV(CADR AD)))THALIST)
13700 (RETURN T)
13750 DE4 (THVAL @(THERASE(THEV(CADR AD)))THALIST)
13800 (REMPROP(CADR AD)@THEOREM)
13850 (PUTPROP(CADR AD)(CADDR AD)@THEOREM)
13900 (THVAL @(THASSERT(THEV(CADR AD)))THALIST)
13950 (RETURN T)
14000 DE5 (THVAL @(THERASE(THEV(CADR AD)))THALIST)
14050 (RETURN T)
14100 DE6 (SETQ TE(COND((EQ(CADDR AD)@TO)(READLIST(APPEND @(R T)(EXPLODE(CADR AD)))))
14150 (T(READLIST(APPEND @(R F)(EXPLODE(CADR AD)))))))
14200 (SET TE(DELRL(EVAL TE)(CADDDR AD)))
14250 (RETURN T) ))
14300 EXPR)
14350
14400
14410
14420 (DEFPROP FILTERAX
14430 (LAMBDA(THM)
14440 (GET THM @AX) )
14445 EXPR)
14450
14500 (DEFPROP FILTEROP
14550 (LAMBDA(THM)
14600 (AND
14650 (OR(NOT(GET(CAAAR CT )@AX))(GET THM @AX))
14700 (OR(GET(CAAAR CT )@REC)(NOT(EQ(CAAAR CT )THM)))
14750 (OR(NULL(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT ))))))
14800 (MEMQ THM(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT )))))))
14850 (OR(NULL(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT ))))))
14900 (NOT(MEMQ THM(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT )))))))) ) )
14950 EXPR)
15000
15050
15100
15150
15200 (DEFPROP FBODY
15250 (LAMBDA(B)
15300 (COND((OR(EQ(CAAR(CDDDR B))@THGOAL)(AND(EQ(CAAR(CDDDR B))@THOR)
15350 (EQ(CAADAR(CDDDR B))@THAND)))
15400 (CDDR B))
15450 (T(FBODY(CDR B)))) )
15500 EXPR)
15550
15600
15650
15700 (DEFPROP OPTIM
15750 (LAMBDA(PLN)
15800 (PROG(OPLN SUL)
15850 (SETQ OPLN(OPDEAD PLN PLN))
15900
15950
16000 OP3 (COND((NULL SUL)(RETURN OPLN)))
16050 (SETQ OPLN(SUBST(CAAR SUL)(CDAR SUL)OPLN))
16100 (SETQ GOL(SUBST(CAAR SUL)(CDAR SUL)GOL))
16150 (SETQ SUL(CDR SUL))
16200 (GO OP3) ))
16250 EXPR)
16300
16350
16400 (DEFPROP OPDEAD
16450 (LAMBDA(PLNA PLN)
16500 (COND((ATOM PLNA)PLNA)
16550 ((AND(EQ @←(CAR PLNA))(NOT(XRH(CADR PLNA)PLN))(NOT(XNA(CADR PLNA)PLN))
16600 (COND((ATOM(CADDR PLNA))(SETQ SUL(CONS(CONS(CADDR PLNA)(CADR PLNA))SUL)))
16650 (T T)) )
16700 NIL)
16750 (T(APPEND(CLIST(OPDEAD(CAR PLNA)PLN))(OPDEAD(CDR PLNA)PLN)))) )
16800 EXPR)
16850
16900
16950 (DEFPROP CLIST
17000 (LAMBDA(X)
17050 (COND((NULL X)NIL)
17100 (T(LIST X))))
17150 EXPR)
17200
17250
17300 (DEFPROP XRH
17350 (LAMBDA(X P)
17400 (COND((ATOM P)NIL)
17450 ((EQ @←(CAR P))(SUBSTP(CADDR P)X))
17500 (T(OR(XRH X(CAR P))(XRH X(CDR P))))))
17550 EXPR)
17600
17650
17700 (DEFPROP XNA
17750 (LAMBDA(X P)
17800 (COND((EQ X P)T)
17850 ((ATOM P)NIL)
17900 ((EQ @←(CAR P))NIL)
17950 (T(OR(XNA X(CAR P))(XNA X(CDR P))))))
18000 EXPR)
18050
18100 (DEFPROP TSLPLAN
18150 (LAMBDA(P)
18200 (PROG(PL SEMCOL)
18250 (SETQ PL P)
18300 (COND((NULL PL)(RETURN NIL)))
18350 (SETQ INDENT(CONS @" " INDENT))
18400 (TERPRI)
18450 (PRINDENT INDENT)
18500 (PRINC @BEGIN)(TERPRI)
18550 T1 (PRINDENT INDENT)
18600 (TSLPLANI(CAR PL))
18650 (SETQ PL(CDR PL))
18700 (COND((NOT(NULL PL))(GO T1)))
18750 (PRINDENT INDENT)
18800 (PRINC @END)(TERPRI)
18850 (SETQ INDENT(CDR INDENT))
18900 (RETURN T) ))
18950 EXPR)
19000
19050
19100 (DEFPROP TSLPLANI
19150 (LAMBDA(PI)
19200 (PROG(PIT)
19250 (SETQ PIT PI)
19300 (COND((EQ(CAR PIT)@IF)(GO TS3))
19350 ((EQ(CAR PIT)@WHILE)(GO TS6))
19400 ((EQ(CAR PIT)@←)(GO TS9)) )
19450 (PRINC(CAR PIT))
19500 (COND((NULL(CDR PIT))(PRINC @;)(TERPRI)(RETURN T)))
19550 (PRINC(CDR PIT))
19600 (GO TS13)
19650 TS3 (SETQ PIT(CDR PIT))
19700 (PRINC @"IF ")
19750 (TSTCOND(CAR PIT))
19800 (SETQ PIT(CDR PIT))
19850 (PRINC @" THEN ")
19900 (SETQ PIT(CDR PIT))
19950 (COND((CDR PIT)(SETQ SEMCOL T)))
20000 (SETQ INDENT(CONS @" " INDENT))
20050 (TERPRI) (PRINDENT INDENT)
20100 (TSLPLANI(CAR PIT))
20150 (SETQ PIT(CDR PIT))
20200 (SETQ INDENT(CDR INDENT))
20250 (COND((NULL PIT)(RETURN T)))
20300 (SETQ PIT(CDR PIT))
20350 (PRINDENT INDENT)
20400 (PRINC @"ELSE ")
20450 (COND((AND(ATOM(CAAR PIT))(NOT SEMCOL))(TSLPLANI(CAR PIT))(GO TS13))
20500 ((ATOM(CAAR PIT))(TSLPLANI(CAR PIT))(RETURN T))
20550 (T(TSLPLAN(CAR PIT))(RETURN T)))
20600 TS6 (SETQ PIT(CDR PIT))
20650 (PRINC @"WHILE ")
20700 (TSTCOND(CAR PIT))
20750 (SETQ PIT(CDDR PIT))
20800 (PRINC @" DO ")
20850 (TSLPLAN(CAR PIT))
20900 (RETURN T)
20950 TS9 (SETQ PIT(CDR PIT))
21000 (PRINC(CAR PIT))
21050 (PRINC @" ← ")
21100 (SETQ PIT(CDR PIT))
21150 (COND((ATOM(CAR PIT))(GO TS11)))
21200 (COND((NOT(FUNDEF(CAR PIT)T))(GO TS13)))
21250 (PRINC(CAAR PIT))
21300 (COND((NULL(CDAR PIT))(GO TS13)))
21350 (COND((ATOM(CADAR PIT))(PRINC(CDAR PIT)))
21400 (T(PRINC(CADAR PIT))))
21450 (GO TS13)
21500 TS11 (PRINC(CAR PIT))
21550 TS13 (COND((NOT SEMCOL)(PRINC @;))) (TERPRI)
21600 (RETURN T) ))
21650 EXPR)
21700
21750
21800 (DEFPROP FUNDEF
21850 (LAMBDA(FU SW)
21900 (PROG(FFL FAL AAL EAAL)
21950 (SETQ FFL(ASSOC(CAR FU)FUNDEFLIST))
22000 (COND((NULL FFL)(RETURN FU)))
22050 (SETQ FAL(CADR FFL))
22100 (SETQ FFL(CADDR FFL))
22150 (SETQ AAL(CDR FU))
22200 FU3 (COND((ATOM(CAR AAL))(SETQ EAAL(CAR AAL)))
22250 (T(SETQ EAAL(FUNDEF(CAR AAL)NIL))))
22300 (SETQ FFL(SUBST EAAL (CAR FAL)FFL))
22350 (SETQ AAL(CDR AAL))
22400 (SETQ FAL(CDR FAL))
22450 (COND(FAL(GO FU3)))
22500 (COND(SW(MAPC(FUNCTION NPRINC)FFL))
22550 (T(RETURN FFL)))
22600 (RETURN NIL) ))
22650 EXPR)
22700
22750
22800
22850 (DEFPROP NPRINC
22900 (LAMBDA(FF)
22950 (COND((ATOM FF)(PRINC FF))
23000 (T(MAPC(FUNCTION NPRINC)FF))) )
23050 EXPR)
23100
23150
23200 (DEFPROP PRINDENT
23250 (LAMBDA(I)
23300 (PROG(II)
23350 (SETQ II I)
23400 PR4 (PRINC(CAR II))
23450 (SETQ II(CDR II))
23500 (COND((NULL II)(RETURN T))
23550 (T(GO PR4))) ))
23600 EXPR)
23650
23700
23750 (DEFPROP TSTCOND
23800 (LAMBDA(C)
23850 (PROG(CC CC1)
23900 (SETQ CC C)
23910 TS0 (COND((ATOM(CAR C))(SETQ CC1 CC))
23914 (T(SETQ CC1(CAR CC))))
23950 (COND((NOT(EQ NEGSGN(CAR CC1)))(GO TS2)))
24000 (PRINC NEGSGN)
24050 (SETQ CC1(CDR CC1))
24100 TS2 (PRINC(CAR CC1))
24150 (PRINC(CDR CC1))
24160 (SETQ CC(CDR CC))
24164 (COND((OR(ATOM(CAR C))(NULL CC))(RETURN T)))
24168 (PRINC @" ")(PRINC @∧)(PRINC @" ")
24172 (GO TS0) ))
24200 EXPR)
24250
24300 (DEFPROP UNCERTLIT
24350 (LAMBDA(LI DSW LI1 LI2)
24400 (PROG NIL
24450 (SETQ UNCERTLIST(APPEND UNCERTLIST(LIST LI)))
24500 (RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI1 @X)))
24550 (RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI2 @X)))
24600 (COND(DSW(RETURN NIL))
24650 (T(RETURN T))) ))
24700 EXPR)
24750
24800 (DEFPROP FINDINSTANG
24850 (LAMBDA(CTH)
24900 (COND((NULL CTH)NIL)
24950 ((NULL(CDR CTH))(RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))GOL)
25000 ((NOT(SUBSTP(CAR(CDAADR CTH))@THV))
25050 (RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))
25100 (CAR(CDAADR CTH)))
25150 (T(FINDINSTANG(CDR CTH)))) )
25200 EXPR)
25250
25300 (DEFPROP CONDSTAT
25350 (LAMBDA(G DSW)
25400 (PROG (TE GL PRLIST)
25450 (COND((AND(NULL UNCERTLIST)DSW)(RETURN NIL))
25500 ((NULL UNCERTLIST)(RETURN T)))
25550 (COND((NOT(SUBSTP G @THV))(SETQ GL G)(RPLACA CT(CONS(CAAR CT)(CONS @IF(CDAR CT)))))
25600 (T(SETQ GL(FINDINSTANG CT))))
25650 (SETQ SSW T)
25700 (SETQ TE(CONS(APPEND(LIST @IF(TSTLIT2(CAR UNCERTLIST)) @THEN)
25850 (LIST(NESTIF(LIST(CAR UNCERTLIST))(CDR UNCERTLIST)GL))@(ELSE))(EVAL(CAR(THV ANS)))))
25900 (THSET(CAR(THV ANS))TE)
25950 (THASSERT(THEV(CAR UNCERTLIST)))
25975 (THSETQ(THV PASSUM)(CONS(CAR UNCERTLIST)(THV PASSUM)))
26000 (SETQ UNCERTLIST NIL)
26050 (THSETQ(THV PROCLIST)(CONS PRLIST(THV PROCLIST)))
26100 (THSETQ(THV ANS)(CONS(LIST @THV(GENSYM))(THV ANS)))
26150 (THVSET(CAR(THV ANS))NIL)
26200 (SETQ SSW NIL)
26250 (RETURN T) ))
26300 EXPR)
26350
26400
26450 (DEFPROP NESTIF
26500 (LAMBDA(FL TL GL)
26550 (COND((NULL TL)(PROCALL FL TL GL))
26600 (T(APPEND(LIST @IF(TSTLIT2(CAR TL))@THEN)
26750 (LIST(NESTIF(CONS(CAR TL)FL)(CDR TL)GL))
26800 (LIST @ELSE (PROCALL FL TL GL))))))
26850 EXPR)
26900
26950
27000 (DEFPROP PROCALL
27050 (LAMBDA(FL TL GL)
27100 (PROG(PL ST PFL LI QFL)
27150 (SETQ PFL FL)
27200 (SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
27250 (SETQ PRLIST(CONS PL PRLIST))
27300 (SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
27350 (COND(TL(THVAL @(THASSERT(THEV(CAR TL)))THALIST)))
27400 PR2 (SETQ LI(CAR PFL))
27450 (COND((EQ @N(CAR(EXPLODE(CAR LI))))
27500 (SETQ LI(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR LI))))
27550 (T(SETQ LI(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI)))))
27600 (SETQ QFL(CONS LI QFL))
27650 (THASSERT(THEV LI))
27700 (SETQ PFL(CDR PFL))
27750 (COND(PFL(GO PR2)))
27800 (EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
27850 (THDUMP)
27900 (OUTC NIL)
27950 PR4 (THERASE(THEV(CAR QFL)))
28000 (SETQ QFL(CDR QFL))
28050 (COND(QFL(GO PR4)))
28100 (COND(TL(THVAL @(THERASE(THEV(CAR TL)))THALIST)))
28150 (SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GL ST))))
28160 (THSETQ(THV COMMENTLIST)(CONS(LIST PL @ATTEMPTS_TO_ACHIEVE_
28162 (TSTLIT GL))(THV COMMENTLIST)))
28200 (RETURN(APPEND(LIST PL)(CDR(TSTLIT GL)))) ))
28250 EXPR)
28300
28350 (DEFPROP INSTANTHV
28400 (LAMBDA(LL)
28450 (COND((NULL LL)NIL)
28500 ((ATOM LL)LL)
28550 ((EQ(CAR LL)@THV)(THVAL LL THALIST))
28600 (T(CONS(INSTANTHV(CAR LL))(INSTANTHV(CDR LL))))))
28650 EXPR)
28700
28750
28800 (DEFPROP DISPOST
28850 (LAMBDA(DNF)
28900 (PROG(TE PRLIST)
28950 (SETQ SSW T)
29000 (SETQ DNF(INSTANTHV DNF))
29050 (SETQ TE(CONS(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DNF)(APPEND(CDDR DNF)(LIST(CAR DNF)))))@THEN)
29100 (LIST(NESTIFP(LIST(CAR DNF))(CDR DNF)(CAAR DNF))))
29150 (EVAL(CAR(THV ANS)))))
29200 (THSET(CAR(THV ANS))TE)
29250 (THSETQ(THV PROCDATA)(CONS(LIST PRLIST(THV DBLITS)(THV ASSERTLITS))
29300 (THV PROCDATA)))
29350 (SETQ SSW NIL)
29400 (RETURN T) ))
29450 EXPR)
29500
29550
29600 (DEFPROP NESTIFP
29650 (LAMBDA(ADF DF GLP)
29700 (COND((NULL(CDR DF))(PROCALLP(APPEND DF ADF) GLP))
29750 (T(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DF)(APPEND(CDDR DF)(CONS(CAR DF)ADF))))@THEN)
29800 (LIST(NESTIFP(CONS(CAR DF)ADF)(CDR DF)GLP))
29850 (LIST @ELSE(PROCALLP (APPEND DF ADF) GLP))))) )
29900 EXPR)
29950
30000
30050 (DEFPROP TSTLIT
30100 (LAMBDA(LI)
30150 (COND((EQ @R(CAR(LAST LI)))(REVERSE(CDR(REVERSE LI))))
30200 (T LI)) )
30250 EXPR)
30300
30350
30400 (DEFPROP PROCALLP
30450 (LAMBDA(DF GLP)
30500 (PROG(PL ST CL SSW CLL)
30510 (SETQ CLL DF)
30550 (SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
30600 (SETQ PRLIST(CONS PL PRLIST))
30650 (SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
30700 (SAVESTATE @XXXX)
30750 (THFLUSH THASSERTION THERASING THCONSE)
30800 (DSKIN CURSTATE)
30850 (COND((NULL DF)(GO PR7)))
30900 PR1 (SETQ CL(CAR CLL))
30910 PR3 (ASSERTPOST(CAR CL)SSW)
30920 (SETQ CL(CDR CL))
30930 (COND(CL(GO PR3)))
30940 (SETQ SSW T)
30950 (SETQ CLL(CDR CLL))
30960 (COND(CLL(GO PR1)))
31100 PR7 (EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
31150 (THDUMP)(OUTC NIL)
31200 (SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GLP ST))))
31250 (THFLUSH THASSERTION THERASING THCONSE)
31300 (DSKIN XXXX)
31310 (THSETQ(THV COMMENTLIST)(CONS(LIST PL @ATTEMPTS_TO_ACHIEVE_
31312 (TSTLIT GLP))(THV COMMENTLIST)))
31350 (RETURN(APPEND(LIST PL)(CDR(TSTLIT GLP)))) ))
31400 EXPR)
31450
31500
31550 (DEFPROP SAVESTATE
31600 (LAMBDA(SS)
31650 (PROG NIL
31700 (EVAL(LIST @OUTC(LIST @OUTPUT @DSK: SS)T))
31750 (THDUMP)
31800 (OUTC NIL) (RETURN T) ))
31850 EXPR)
31900
31910 (DEFPROP TSTLIT2
31913 (LAMBDA(LI)
31916 (PROG(LIT)
31919 (COND((EQ @R(CAR(LAST LI)))
31922 (SETQ LIT(REVERSE(CDR(REVERSE LI))))))
31925 (COND((EQ NEGSGN(CAR LI))
31928 (SETQ LIT(CDR LIT)))
31931 ((EQ @N(CAR(EXPLODE(CAR LI))))
31934 (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR LIT))))
31937 (T(SETQ LIT(CONS NEGSGN LIT))))
31940 (RETURN LIT) ))
31943 EXPR)
31946
31949
31950 (DEFPROP PTESTLITS
31953 (LAMBDA(PO NEG)
31956 (COND((NULL NEG)(LIST(TSTLIT(CAR PO))))
31959 (T(CONS(TSTLIT2(CAAR NEG))(PTESTLITS PO(CDR NEG))))))
31962 EXPR)
31965
31968
31971 (DEFPROP NRTSTLITS
31974 (LAMBDA(LL)
31977 (COND((MEMBER(CAR(LAST LL))(CDR(REVERSE LL)))
31980 (CDR(REVERSE LL)))
31983 (T(REVERSE LL))))
31986 EXPR)
31989
31992
31995 (DEFPROP ASSERTPOST
31998 (LAMBDA(LI SW)
32001 (PROG(NSW LIT PSW)
32004 (COND((EQ @N(CAR(EXPLODE(CAR LI))))
32007 (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR LI)))
32010 (SETQ NSW T))
32013 (T(SETQ LIT LI)))
32016 (COND((GET(CAR LIT)@PARTIAL)(SETQ PSW T)))
32019 (COND((OR(AND NSW PSW(NOT SW))
32022 (AND(NOT NSW)PSW(NOT SW))
32025 (AND(NOT NSW)(NOT PSW)(NOT SW))
32028 (AND NSW(NOT PSW)SW))
32031 (THASSERT(THEV(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI))))))
32034 (RETURN T) ))
32037 EXPR)
32040
32043
32050
32100
32150 (DEFPROP ELSECLAUSE
32200 (LAMBDA NIL
32250 (PROG(CB IFS)
32300 (SETQ IFS(CDAR CT))
32350 (THSETQ CT(CDR CT)T T)
32400 EL2 (SETQ CB(REVERSE(EVAL(CAR(THV ANS)))))
32450 (THSETQ(THV ANS)(CDR(THV ANS)))
32500 (THSET(CAR(THV ANS))(CONS(APPEND(CAR(EVAL(CAR(THV ANS))))
32550 (LIST CB))
32600 (CDR(EVAL(CAR(THV ANS))))) )
32650 (SETQ GANS(REVERSE(EVAL(CAR(THV ANS)))))
32700 (THSETQ(THV PROCDATA)(CONS(LIST(CAR(THV PROCLIST))(THV DBLITS)(THV ASSERTLITS))
32750 (THV PROCDATA)))
32800 (THSETQ(THV PROCLIST)(CDR(THV PROCLIST))T T)
32850 (SETQ IFS(CDR IFS))
32900 (COND((ATOM(CAR IFS))(GO EL2)))
32950 (RETURN T) ))
33000 EXPR)
33050
35600
35650
35700 (DEFPROP SUBPLANL
35750 (LAMBDA(P PL)
35800 (COND((NULL PL)P)
35850 (T(SUBPLANL(SUBPLANL1 P(CAR PL))(CDR PL)))))
35900 EXPR)
35950
36000
36050 (DEFPROP SUBPLANL1
36100 (LAMBDA(P PL)
36150 (COND((ATOM P)P)
36200 ((AND(NOT(ATOM(CAR P)))(EQ @←(CAAR P))(EQ(CAADDR(CAR P))(CAAR PL)))
36250 (SUBPLANL1(APPEND(REVERSE(SUBPLANL2(CAR P)PL))(CDR P))PL))
36300 (T(CONS(SUBPLANL1(CAR P)PL)(SUBPLANL1(CDR P)PL)))))
36350 EXPR)
36400
36450
36500 (DEFPROP SUBPLANL2
36550 (LAMBDA(P PL)
36600 (PROG(PT PLT BOD)
36625 (PRINT @L36625)(PRINT P)(PRINT PL)
36650 (SETQ PT P)(SETQ PLT PL)
36700 (SETQ BOD(CADR PLT))
36750 (SETQ BOD(SUBST(CADR PT)(CADAR PLT)BOD))
36800 (SETQ PT(CDADDR PT))
36850 (SETQ PLT(CDDAR PLT))
36900 SU2 (COND((NULL PT)(RETURN BOD)))
36950 (SETQ BOD(SUBST(CAR PT)(CAR PLT)BOD))
37000 (SETQ PT(CDR PT))
37050 (SETQ PLT(CDR PLT))
37100 (GO SU2) ))
37150 EXPR)
37160
37163 (DEFPROP DELL
37166 (LAMBDA(C L)
37169 (COND((NULL L)NIL)
37172 ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
37175 (EQUAL(CADR C)(CADAR L))
37178 (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
37181 (T T)))
37184 (CDR L))
37187 ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
37190 (COND((CADR C)(EQUAL(CADR C)(CADAR L)))
37193 (T T)))
37196 (CDR L))
37199 (T(CONS(CAR L)(DELL C(CDR L))))) )
37202 EXPR)
37205
37208
37211 (DEFPROP FINDC
37214 (LAMBDA(C L)
37217 (COND((NULL L)NIL)
37220 ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
37223 (EQUAL(CADR C)(CADAR L))
37226 (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
37229 (T T)))
37232 (CAR L))
37235 ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
37238 (COND((CADR C)(EQUAL(CADR C)(CADAR L1)))
37241 (T T)))
37244 (CAR L))
37247 (T(FINDC C(CDR L)))) )
37250 EXPR)
37253
37255 (DEFPROP ELEVA
37257 (LAMBDA(C L)
37259 (COND((NULL L)NIL)
37261 ((AND(NULL(CDDAR L))(EQUAL(CAAR C)(CADAAR L)))
37263 (SETQ SW T)(CONS(LIST(CAAR L)(NRCONJ(CADAR L)(CADR C)))
37265 (CDR L)))
37267 (T(CONS(CAR L)(ELEVA C(CDR L))))) )
37269 EXPR)
37271
37273
37275 (DEFPROP ELEVB
37277 (LAMBDA(C L)
37279 (COND((NULL L)NIL)
37281 ((AND(NULL(CDDAR L))(EQUAL(CADAR C)(CAAAR L)))
37283 (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
37285 (CDR L))
37287 (T(CONS(CAR L)(ELEVB C(CDR L))))) )
37289 EXPR)
37291
37293
37295 (DEFPROP ELEVC
37297 (LAMBDA(C L)
37299 (COND((NULL L)NIL)
37301 ((AND(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L)))
37303 (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
37305 (SETQ SW T)
37307 (CDR L))
37309 (T(CONS(CAR L)(ELEVC C(CDR L))))) )
37311 EXPR)
37313
37315
37317 (DEFPROP NRCONJ
37319 (LAMBDA(R1 R2)
37321 (COND((NULL R2)R1)
37323 ((MEMBER(CAR R2)R1)(NRCONJ R1(CDR R2)))
37325 (T(CONS(CAR R2)(NRCONJ R1(CDR R2))))) )
37327 EXPR)
37329
37331
37345 (DEFPROP WHILASSEM
37350 (LAMBDA(BP IP CL CT )
37400 (PROG(ALP ALS PA Y Z W R SASG SASGR TE ALF BET WFT ALFT RP)
37410 (PRINT @L37410)(PRINT BP)(PRINT IP)(PRINT CL)(PRINT CT)
37415 (PRINT @L37415)(PRINT(THV SASSERTLITS))(PRINT(THV ASSERTLITS))
37423 (SETQ WFT(THV FT))
37425 (PRINT @L37425)(PRINT CL)(PRINT WFT)
37427 (SETQ IP(REVERSE IP))
37431 WH2 (SETQ PA(CAR CL))
37432 (PRINT @L37432)(PRINT PA)(PRINT WFT)
37435 (SETQ Y(READLIST(APPEND(LIST @Y)(EXPLODE(THSETQ(THV YN)(ADD1(THV YN)))))))
37437 (SETQ Z(READLIST(APPEND(LIST @Z)(EXPLODE(THSETQ(THV ZN)(ADD1(THV ZN)))))))
37440 (COND((CDDR PA)(SETQ ALF(CAR PA))(SETQ BET(CADR PA)))
37443 (T(SETQ ALF(CAAR PA))(SETQ BET(CADAR PA))))
37444 (SETQ ALFT(COND((CDDAR WFT)(CAAR WFT))(T(CAAAR WFT))))
37446 (SETQ BP(CONS(LIST @← Y ALFT)BP))
37447 (SETQ LIFOL(CONS(COND((THASVAL(THV NT))(SUBST Y ALFT(SUBST Z ALF(CAR LIFOL) )))
37448 (T(SUBST Y ALFT(SUBST Z BET(CAR LIFOL))))) (CDR LIFOL)))
37449 (SETQ IP(APPEND IP(LIST(LIST @← Y Z))))
37452 (SETQ ALP(CONS(CONS ALF Y)ALP))
37455 (SETQ ALS(CONS(CONS BET Z)ALS))
37456 (PRINT @L37456)(PRINT PA)
37458 (COND((CDDR PA)(SETQ SASG(APPEND(LIST(LIST @← Z(CADDR PA)))
37461 SASG))(GO WH4)))
37464 (SETQ R(CADR PA))
37467 (SETQ R(APPEND(LIST(CAR R))(COND((CDR R)(COND((CDDR R)(LIST @∧ (CADR R) @∧ (CADDR R)))
37470 (T(LIST @∧ (CADR R)))))
37473 (T NIL))))
37475 (SETQ W(READLIST(APPEND(LIST @W)(EXPLODE(THV ZN)))))
37477 (SETQ RP R)
37478 (SETQ R(SUBST W BET R))
37479 (COND((EQUAL R RP)(SETQ R(SUBST W ALF R))))
37481 (SETQ SASGR(APPEND (LIST(LIST @IF R @THEN(LIST @← Z W)))SASGR))
37482 WH4 (SETQ CL(CDR CL))
37483 (SETQ WFT(CDR WFT))
37485 (COND(CL(GO WH2)))
38525 (PRINT @L38525)(PRINT ALP)(PRINT ALS)(PRINT SASG)(PRINT SASGR)
38530 (SETQ ALP(DEQ ALP))
38533 (SETQ ALS(DEQ ALS))
38550 (SETQ SASG(REVERSE(VSUB ALP SASG)))
38575 (SETQ SASGR(REVERSE(VSUB ALP SASGR)))
38600 (SETQ IP(VSUB ALS IP))
38625 (SETQ IP(VSUB ALP IP))
38650 (SETQ CT(VSUB ALP CT))
38700 (SETQ TE(SUBPLANL(APPEND(LIST(LIST @WHILE(CONS NEGSGN CT)@DO(APPEND SASG IP SASGR)))(APPEND SASGR BP))(THV PLANL)))
38712 (PRINT TE)
38725 (RETURN TE) ))
38750 EXPR)
38752
38754
38756 (DEFPROP DEQ
38758 (LAMBDA(SAL)
38760 (COND((NULL SAL)NIL)
38762 (T(CONS(CAR SAL)(DEQ(DEQ1(CAR SAL)(CDR SAL)))))))
38764 EXPR)
38766
38768 (DEFPROP DEQ1
38770 (LAMBDA(A D)
38772 (COND((NULL D)NIL)
38774 ((EQUAL(CAR A)(CAAR D))(DEQ1 A(CDR D)))
38776 (T(CONS(CAR D)(DEQ1 A(CDR D))))))
38778 EXPR)
38780
38796
38808 (DEFPROP COMPCHANGES
38811 (LAMBDA(IN1 IN2 ACL)
38814 (PROG(CL1 L1 L2 UL UA A1 A2 LCL SREL SW CREL)
38815 (PRINT @L38815)(PRINT ACL)(PRINT IN1)(PRINT IN2)
38817 CO2 (SETQ L1(CAR IN1)) (SETQ L2(CAR IN2))
38820 (SETQ UL(ELASSOC L2 ACL))
38821 (SETQ LCL NIL)
38822 (SETQ CREL(COND((EQ @R(CAR(REVERSE L1)))(REVERSE(CDR(REVERSE L1))))
38823 (T L1)))
38824 (SETQ L1(CDR L1)) (SETQ L2(CDR L2))
38826 (COND((EQUAL L1 L2)(GO CO8)))
38829 CO4 (SETQ A1(CAR L1)) (SETQ A2(CAR L2)) (SETQ SW NIL)
38832 (SETQ UA(COND(UL(CAR UL))(T NIL)))
38834 (PRINT @L38834)(PRINT CL1)(PRINT LCL)(PRINT A1)(PRINT A2)(PRINT UA)
38835 (COND((EQUAL A1 A2)(GO CO6)))
38838 (COND((AND(NULL UA)(OR(NOT(EQUAL(SUBST @# A1 A2)A2))
38841 (NOT(EQUAL(SUBST @# A2 A1)A1))))
38844 (GO CO6)))
38847 (COND((AND UA(ATOM UA)(NOT(EQUAL(SUBST @# A1 A2)A2)))
38850 (COND((AND(NOT(FINDC(LIST A1 A2 NIL)CL1))
38853 (NOT(FINDC(LIST A1 A2 NIL)LCL)))
38856 (SETQ LCL(CONS(LIST A1 A2 A2)LCL))
38859 (GO CO6))
38862 (T(GO CO6))) ))
38865 (COND((AND UA(ATOM UA))(GO CO6)))
38868 (COND((AND(NOT(ATOM UA))(NOT(MEMBER(LIST A1 A2 UA)CL1))
38871 (NOT(MEMBER(LIST A1 A2 UA)LCL)))
38874 (SETQ CL1(DELL(LIST A1 A2 NIL)CL1))
38877 (SETQ CL1(DELL(LIST(LIST A1 A2)NIL)CL1))
38880 (SETQ LCL(DELL(LIST A1 A2 NIL)LCL))
38883 (SETQ LCL(CONS(LIST A1 A2 UA)LCL))
38886 (GO CO6)))
38889 (COND((AND(NULL UA)(OR(FINDC(LIST A1 A2 NIL)CL1)
38892 (FINDC(LIST(LIST A1 A2)(LIST CREL))CL1)))
38895 (GO CO6)))
38898 (COND((NULL UA)(SETQ SREL (LIST CREL)))
38901 (T(GO CO6)))
38904 (SETQ CL1(ELEVA(LIST(LIST A1 A2)SREL)CL1))
38907 (COND(SW(GO CO6)))
38910 (SETQ LCL(ELEVA(LIST(LIST A1 A2)SREL)LCL))
38913 (COND(SW(GO CO6)))
38916 (SETQ CL1(ELEVB(LIST(LIST A1 A2)SREL)CL1))
38919 (SETQ LCL(ELEVB(LIST(LIST A1 A2)SREL)LCL))
38922 (SETQ CL1(ELEVC(LIST(LIST A1 A2)SREL)CL1))
38925 (SETQ LCL(ELEVC(LIST(LIST A1 A2)SREL)LCL))
38928 (COND(SW(SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))(GO CO6)))
38929 (SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))
38931 CO6 (SETQ L1(CDR L1)) (SETQ L2(CDR L2))
38934 (COND(UL(SETQ UL(CDR UL))))
38937 (COND(L1(GO CO4)))
38940 (SETQ CL1(APPEND LCL CL1))
38943 CO8 (SETQ IN1(CDR IN1))
38946 (SETQ IN2(CDR IN2))
38947 (COND(IN1(GO CO2)))
38948 (RETURN CL1) ))
38949 EXPR)
38950 (DEFPROP REM#
39000 (LAMBDA(A)
39050 (COND((ATOM A)A)
39100 ((EQ @#(CAR A))(CADDR A))
39150 (T(CONS(REM#(CAR A))(REM#(CDR A))))))
39200 EXPR)
39250
39255
39257 (DEFPROP AMBIG
39259 (LAMBDA(CHL)
39261 (COND((NULL CHL)NIL)
39263 ((AMBIG1(CAR CHL)(CDR CHL))T)
39265 (T(AMBIG(CDR CHL)))) )
39267 EXPR)
39269
39271 (DEFPROP AMBIG1
39273 (LAMBDA(AC DC)
39275 (COND((NULL DC)NIL)
39277 ((AMBIG2(AMBIG3 AC)(AMBIG3(CAR DC)))T)
39279 (T(AMBIG1 AC(CDR DC)))) )
39281 EXPR)
39283
39285 (DEFPROP AMBIG2
39287 (LAMBDA(P1 P2)
39289 (OR(EQUAL(CAR P1)(CAR P2)) (EQUAL(CADR P1)(CADR P2))
39291 (EQUAL(CAR P1)(CADR P2))(EQUAL(CADR P1)(CAR P2)) ) )
39293 EXPR)
39295
39297 (DEFPROP AMBIG3
39299 (LAMBDA(C)
39301 (COND((CDDR C)(LIST(CAR C)(CADR C)))
39302 (T(CAR C))) )
39303 EXPR)
39304
39305 (DEFPROP REMBT
39306 (LAMBDA(A)
39309 (PROG NIL
39310 (GO RE1)
39312 (THDO(PRED1ARG P1A))
39315 (THDO(PRED2ARG P2A))
39318 (THDO(PRED3ARG P3A))
39321 (THDO(PRED4ARG P4A))
39324 (THDO(PRED5ARG P5A))
39327 RE1 (RETURN(REM# A)) ))
39330 EXPR)
39333
39336
39339 (DEFPROP PRED1ARG
39342 (LAMBDA(X)
39345 (THPROG(P)
39348 (THAMONG(THV P)X)
39351 A (THFIND ALL
39354 (THEV(THDO
39357 (THERASE((THV P)(THV Y1)))
39360 (THASSERT((THV P)(THEV(CADDR(THV Y1))))) ))
39363 (Y1)
39366 (THGOAL((THV P)(THNV Y1)))
39369 (EQ @#(CAR(THV Y1))) )
39372 (THFINALIZE THTAG A)
39375 (THFAIL) ))
39378 EXPR)
39381
39384
39387 (DEFPROP PRED2ARG
39390 (LAMBDA(X)
39393 (THPROG(P)
39396 (THAMONG(THV P)X)
39399 A (THFIND ALL
39402 (THEV(THDO
39405 (THERASE((THV P)(THV Y1)(THV Y2)))
39408 (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39411 (THEV(CHECK#(THV Y2))) )) ))
39414 (Y1 Y2)
39417 (THGOAL((THV P)(THNV Y1)(THNV Y2)))
39420 (THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))) )
39423 (THFINALIZE THTAG A)
39426 (THFAIL) ))
39429 EXPR)
39432
39435
39438 (DEFPROP PRED3ARG
39441 (LAMBDA(X)
39444 (THPROG(P)
39447 (THAMONG(THV P)X)
39450 A (THFIND ALL
39453 (THEV(THDO
39456 (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)))
39459 (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39462 (THEV(CHECK#(THV Y2)))
39463 (THEV(CHECK#(THV Y3))) )) ))
39465 (Y1 Y2 Y3)
39468 (THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)))
39471 (THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))) )
39474 (THFINALIZE THTAG A)
39477 (THFAIL) ))
39480 EXPR)
39483
39486
39489 (DEFPROP PRED4ARG
39492 (LAMBDA(X)
39495 (THPROG(P)
39498 (THAMONG(THV P)X)
39501 A (THFIND ALL
39504 (THEV(THDO
39507 (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)))
39510 (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39513 (THEV(CHECK#(THV Y2)))
39516 (THEV(CHECK#(THV Y3)))
39517 (THEV(CHECK#(THV Y4))) )) ))
39519 (Y1 Y2 Y3 Y4)
39522 (THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)))
39525 (THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))) )
39528 (THFINALIZE THTAG A)
39531 (THFAIL) ))
39534 EXPR)
39536
39538
39540 (DEFPROP PRED5ARG
39542 (LAMBDA(X)
39544 (THPROG(P)
39546 (THAMONG(THV P)X)
39548 A (THFIND ALL
39550 (THEV(THDO
39552 (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)(THV Y5)))
39554 (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39556 (THEV(CHECK#(THV Y2)))
39558 (THEV(CHECK#(THV Y3)))
39560 (THEV(CHECK#(THV Y4)))
39561 (THEV(CHECK#(THV Y5))) )) ))
39562 (Y1 Y2 Y3 Y4 Y5)
39564 (THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)(THNV Y5)))
39566 (THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))(EQ @#(CAR(THV Y5)))) )
39568 (THFINALIZE THTAG A)
39570 (THFAIL) ))
39572 EXPR)
39574
39576
39578
39590 (DEFPROP TRSUBSTP
39600 (LAMBDA(PL ELT)
39650 NIL)
39700 EXPR)
39750
39800
39850
39900 (DEFPROP TRSUBST
39950 (LAMBDA(NE OE PL)
40000 (SUBST NE OE PL))
40050 EXPR)
40100
40150
40200
40250 (DEFPROP SUBSTP
40300 (LAMBDA(P V)
40350 (COND((EQUAL P V)T)
40400 ((ATOM P)NIL)
40450 (T(OR(SUBSTP(CAR P)V)(SUBSTP(CDR P)V)))))
40500 EXPR)
40550
40600
40650
41050
41100 (DEFPROP VSUB
41150 (LAMBDA(RL PL)
41200 (PROG(CRL SPL DONE CRL1)
41225 (COND((NULL PL)(RETURN NIL)))
41250 (SETQ CRL RL)
41300 (SETQ SPL PL)
41350 VS1 (COND(DONE(GO VS3)))
41400 (SETQ DONE T)
41450 (SETQ CRL(RECSUB1 CRL CRL))
41500 (GO VS1)
41550 VS3 (COND((NOT DONE)(RETURN SPL)))
41600 (SETQ CRL1 CRL)
41650 (SETQ DONE NIL)
41700 VS5 (COND((NULL CRL1)(GO VS3)))
41750 (COND((OR(SUBSTP SPL(CAAR CRL1))(TRSUBSTP SPL(CAAR CRL1)))(SETQ DONE T)))
41800 (SETQ SPL(TRSUBST(CDAR CRL1)(CAAR CRL1)SPL))
41850 (SETQ CRL1(CDR CRL1))
41900 (GO VS5) ))
41950 EXPR)
42000
42050
42100 (DEFPROP RECSUB1
42150 (LAMBDA(RL1 RL2)
42200 (COND((NULL RL1)RL2)
42250 (T(RECSUB1(CDR RL1)(APPEND(RECSUB2(CAR RL1)RL2)RL2)))) )
42300 EXPR)
42350
42400
42450 (DEFPROP RECSUB2
42500 (LAMBDA(RL11 RL22)
42550 (COND((NULL RL22)NIL)
42600 ((AND(OR(SUBSTP(CAAR RL22)(CAR RL11))(TRSUBSTP(CAAR RL22)(CAR RL11)))(NOT(EQ(CDR RL11)(CDAR RL22))))
42650 ((LAMBDA(S)(COND((MEMBER S RL2)(RECSUB2 RL11(CDR RL22)))
42700 (T(APPEND(SETQ DONE NIL)(LIST S)
42750 (RECSUB2 RL11(CDR RL22))))))
42800 (TRSUBST(CDR RL11)(CAR RL11)(CAR RL22))))
42850 (T(RECSUB2 RL11(CDR RL22)))) )
42900 EXPR)
42950
43000
43050 (OPS (TDNE 612000)(TTCALL 51000))
43100 (LAP TTYIN SUBR)
43150 (TTCALL 2 1)
43200 (CLEARM 0 1)
43250 (TDNE 1 '(C 777777 0 777760))
43300 (POPJ P 0)
43350 (CLEARM 0 1)
43400 (POPJ P 0)
43450 NIL
43500
43550
43600 (DEFPROP CJOINCOND
43650 (LAMBDA NIL
43700 (PROG(PD LDB LA)
43750 JO3 (SETQ LDB(CADAR(THV PROCDATA)))
43800 (SETQ LA(CADDAR(THV PROCDATA)))
43850 (COND((EQUAL(LENGTH LDB)(LENGTH(THV DBLITS)))(PRINT @YES)(GO JO6)))
43900 (SETQ LDB(REVERSE(INCRELIT LDB(REVERSE(THV DBLITS)))))
43950 (SETQ LA(REVERSE(INCRELIT LA(REVERSE(THV ASSERTLITS)))))
44000 (SETQ LDB(DBREF LDB LA))
44050 (SETQ JOINCOND(CONS(LIST(CAAR(THV PROCDATA))LDB)JOINCOND))
44100 JO6 (THSETQ(THV PROCDATA)(CDR(THV PROCDATA))T T)
44150 (COND((THV PROCDATA)(GO JO3)))
44200 (RETURN T) ))
44250 EXPR)
44300
44350
44400 (DEFPROP INCRELIT
44450 (LAMBDA(L B)
44500 (COND((NULL L)B)
44550 (T(INCRELIT(CDR L)(CDR B)))) )
44600 EXPR)
44610
44612
44614 (DEFPROP STORPLIB
44616 (LAMBDA NIL
44618 (PROG(PRO)
44619 (COND((NULL COMPI)(ED T)))
44620 (OUTC @PLIB NIL)
44624 (SETQ PRO(LIST @DEFPROP PL
44626 (APPEND(LIST @THCONSE)
44628 (LIST GVARL)
44630 (LIST(CAR TAS))
44632 (IAS(APPEND TYP STA))
44634 (LIST(LIST @THSET @(CAR(THV ANS))(LIST @APPEND @(EVAL(CAR(THV ANS)))
44636 (LIST @REVERSE(LIST @INSTPROG(LIST @QUOTE PANS)(LIST @QUOTE GVARL) )))))
44638 (OAS TAS))
44640 @THEOREM))
44642 (SPRINT PRO 2 1)
44644 (PRINT(LIST @THASSERT PL))
44646 (OUTC NIL NIL) ))
44648 EXPR)
44650
44652
44654 (DEFPROP IAS
44656 (LAMBDA(IA)
44658 (COND((NULL IA)NIL)
44660 (T(CONS(LIST @THGOAL(CAR IA)@(THTBF THTRUE))(IAS(CDR IA))))) )
44668 EXPR)
44670
44672
44674 (DEFPROP INSTPROG
44676 (LAMBDA(PA VARL)
44678 (COND((NULL VARL)PA)
44680 (T(INSTPROG(SUBST(EVAL(LIST @THV(CAR VARL)))(LIST @THV(CAR VARL))PA)(CDR VARL)))) )
44682 EXPR)
44684
44686
44688
44690 (DEFPROP OAS
44692 (LAMBDA(TAS)
44694 (COND((NULL TAS)NIL)
44696 (T(CONS(LIST @THASSERT(CAR TAS))(OAS(CDR TAS))))) )
44700 EXPR)
44702
44704
44750 (DEFPROP GENERALIZE
44800 (LAMBDA NIL
44850 (PROG (TAS TDB CL VN VA PANS TYP STA TEM TEM1 GPAR GVARL)
44900 (PRINT @IS_THIS_PLAN_USEFUL_ENOUGH_TO_BE_GENERALIZED?*)
44950 (COND((READ)(SETQ GSWI GANS))
45000 (T(GO GE9)))
45050 (PRINT @DO_YOU_WANT_TO_SEE_THE_GENERALIZED_VERSION?*)
45100 (COND((READ)(SETQ GGEN T))(T(SETQ GGEN NIL)))
45150 (SETQ TDB(DBREF(THV DBLITS)(APPEND(THV WASSERTLITS)(THV ASSERTLITS))))
45200 (SETQ TAS(REVERSE(NETASSERT(THV ASSERTLITS))))
45250 (SETQ TEM(APPEND TDB TAS))
45300 GE4 (SETQ CL(APPEND(CONSTL(CDAR TEM))CL))
45350 (SETQ TEM(CDR TEM))
45400 (COND(TEM(GO GE4)))
45410 (SETQ GENAL(REVERSE(CDR(REVERSE(CDR (CAR TAS))))))
45419 (PRINT @L45419)(PRINT GOL)(PRINT TDB)(PRINT TAS) (SETQ GPAR @ALL)
45420 (PRINT @IS_THIS_A_PROCEDURE_WITHOUT_SIDE_EFFECTS?*)
45421 (COND((READ)(SETQ GPAR (CDR(REVERSE(CDR(REVERSE GOL)))))))
45422 (COND((NOT(EQ GPAR @ALL))(SETQ CL GPAR)(SETQ TDB(ELIMLOCALPAR TDB))(SETQ TAS(ELIMLOCALPAR TAS))))
45450 (SETQ GCON(REVERSE CL))
45460 (PRINT @L45460)(PRINT GANS)(PRINT TDB)(PRINT TAS)
45500 (SETQ PANS GANS)
45550 (SETQ VN 0) (SETQ IGTDB TDB) (SETQ IGTAS TAS)
45600 (SETQ GTDB TDB)(SETQ GTAS TAS)(SETQ GVL NIL)(SETQ GTYP NIL)(SETQ GSTA NIL)
45650 GE5 (SETQ VA(LIST @THV(READLIST(APPEND @(V)(EXPLODE(SETQ VN(ADD1 VN)))))))
45700 (SETQ TDB(SUBST VA(CAR CL)TDB))
45750 (SETQ TAS(SUBST VA(CAR CL)TAS))
45800 (SETQ PANS(SUBST VA(CAR CL)PANS))
45850 (SETQ VA(CADR VA))
45860 (SETQ GVARL(CONS VA GVARL))
45900 (SETQ GVL(CONS VA GVL))
45950 (SETQ GTDB(SUBST VA(CAR CL)GTDB))
46000 (SETQ GTAS(SUBST VA(CAR CL)GTAS))
46050 (SETQ GSWI(SUBST VA(CAR CL)GSWI))
46100 (SETQ CL(CDR CL))
46150 (COND(CL(GO GE5)))
46160 (SETQ GENAL(COND((ATOM GTAS)NIL)(T(REVERSE(CDR(REVERSE(CDAR GTAS)))))))
46200 (SETQ TEM TDB) (SETQ TEM1 GTDB)
46250 GE6 (COND((EQ @R(CAR(REVERSE(CAR TEM))))(SETQ STA(CONS(CAR TEM)STA)))
46300 (T(SETQ TYP(CONS(CAR TEM)TYP))))
46350 (COND((EQ @R(CAR(LAST(CAR TEM1))))(SETQ GSTA(CONS(CAR TEM1)GSTA)))
46400 (T(SETQ GTYP(CONS(CAR TEM1)GTYP))))
46450 (SETQ TEM(CDR TEM))
46500 (SETQ TEM1(CDR TEM1))
46550 (COND(TEM(GO GE6)))
46600 (SETQ TAS(REVERSE TAS))
46650 (SETQ GTAS(REVERSE GTAS))
46660 (PRINT @L46660)(PRINT TAS)(PRINT TYP)(PRINT STA)
46700 (STORPLIB)
46750 GE9 (SETQ READY(CONS(CONS(LIST PL GOL ST)(LIST GANS))READY)) ))
46800 EXPR)
46850
46852
46854 (DEFPROP ELIMLOCALPAR
46856 (LAMBDA(TL)
46858 (COND((NULL TL)NIL)
46860 ((HASGLOB(CDAR TL))(CONS(CAR TL)(ELIMLOCALPAR(CDR TL))))
46862 (T(ELIMLOCALPAR(CDR TL)))) )
46864 EXPR)
46866
46868
46870
46872 (DEFPROP HASGLOB
46874 (LAMBDA(LI)
46876 (COND((OR(NULL LI)(EQ(CAR LI)@R))T)
46878 ((AND(NOT(ATOM(CAR LI)))(NOT(NUMBERP(CAAR LI))))(AND(HASGLOB(CAR LI))(HASGLOB(CDR LI))))
46880 ((NOT(MEMBER(CAR LI)CL))NIL)
46882 (T(HASGLOB(CDR LI)))) )
46884 EXPR)
46886
46888
46900
46950 (DEFPROP DBREF
47000 (LAMBDA(DB AS)
47050 (PROG(TD1 TD2)
47100 (SETQ TD1(CARDBLIT DB))
47150 (SETQ TD1(NONREDUN(REVERSE TD1)))
47200 DB2 (COND((NOT(ELASSOC(CAR TD1)AS))
47250 (SETQ TD2(CONS(CAR TD1)TD2))))
47300 (SETQ TD1(CDR TD1))
47350 (COND(TD1(GO DB2)))
47400 (RETURN TD2) ))
47450 EXPR)
47500
47502
47504
47506
47508 (DEFPROP ELASSOC
47510 (LAMBDA(L AL)
47512 (COND((NULL AL)NIL)
47514 ((EQUAL L(CAAR AL))(CADAR AL))
47516 (T(ELASSOC L(CDR AL)))) )
47518 EXPR)
47520
47522
47524
47550
47600 (DEFPROP NETASSERT
47650 (LAMBDA(TA1)
47700 (COND((NULL TA1)NIL)
47750 ((THVAL @(THGOAL(THEV(CAAR TA1))(THTBF FILTERAX))THALIST)
47800 (CONS(CAAR TA1)(NETASSERT(CDR TA1))))
47850 (T(NETASSERT(CDR TA1)))) )
47900 EXPR)
47950
48000
48050
48100 (DEFPROP CONSTL
48150 (LAMBDA(TX)
48200 (COND((NULL TX)NIL)
48250 ((EQ @R(CAR TX))NIL)
48300 ((MEMBER(CAR TX)CL)(CONSTL(CDR TX)))
48350 ((NOT(ATOM(CAR TX)))(APPEND(CONSTL(CDAR TX))(CONSTL(CDR TX))))
48400 (T(CONS(CAR TX)(CONSTL(CDR TX))))))
48450 EXPR)
48500
48550
48600
48650 (DEFPROP CARDBLIT
48700 (LAMBDA(DBL)
48750 (COND((NULL DBL)NIL)
48800 (T(APPEND(CARDBLIT1(CAR DBL))(CARDBLIT(CDR DBL))))))
48850 EXPR)
48900
48950
49000 (DEFPROP CARDBLIT1
49050 (LAMBDA(TDBL)
49100 (COND((NULL TDBL)NIL)
49150 ((ATOM(CAR TDBL))(CARDBLIT1(CDR TDBL)))
49200 (T(CONS(CAADAR TDBL)(CARDBLIT1(CDR TDBL))))))
49250 EXPR)
49300
49350
49400 (DEFPROP NONREDUN
49450 (LAMBDA(DBL)
49500 (PROG(NRL PDBL)
49550 (SETQ PDBL DBL)
49600 NO2 (COND((NOT(MEMBER(CAR PDBL)NRL))
49650 (SETQ NRL(CONS(CAR PDBL)NRL))))
49700 (SETQ PDBL(CDR PDBL))
49750 (COND(PDBL(GO NO2)))
49800 (RETURN(REVERSE NRL)) ))
49850 EXPR)
49900
49950
50000
50050 (DEFPROP OUTANS
50100 (LAMBDA NIL
50150 (PROG(GTYP1 GTYP1 GTAS1 IGTYP IGSTA IGTDB1 COMLST CLST)
50200 (TERPRI)
50250 (PRINT @THE_GOAL_)(PRINC (REVERSE(CDR(REVERSE GOL))))(PRINC @_IS_ATTAINABLE_BY_THE_FOLLOWING_PROGRAM:)
50300 (TERPRI)(TERPRI)
50340 (COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
50350 (PRINC(REVERSE(CDR(REVERSE(CDR GOL)))))
50400 (COND((NULL GSWI)(GO OU41)))
50450 (SETQ IGTDB1 IGTDB)
50500 OU1 (COND((EQ @R(CAR(LAST(CAR IGTDB1))))(SETQ IGSTA(CONS(CAR IGTDB1)IGSTA)))
50550 (T(SETQ IGTYP(CONS(CAR IGTDB1)IGTYP))))
50600 (SETQ IGTDB1(CDR IGTDB1))
50650 (COND(IGTDB1(GO OU1)))
50700 (TERPRI)
50750 OU12 (PRINC(CAAR IGTYP)) (PRINC(CDAR IGTYP)) (PRINC @;)
50800 (SETQ IGTYP(CDR IGTYP))
50850 (COND(IGTYP(GO OU12)))
50900 (PRINT @COMMENT)(PRINT @INPUT_CONDITIONS:)(TERPRI)
50950 (OUTCONDI IGSTA)
51000 (PRINT @OUTPUT_CONDITIONS:)(TERPRI)
51050 (OUTCONDI IGTAS)
51100 (PRINC @;)
51104 OU41 (COND((THV ASSL)(PRINT @COMMENT)
51107 (PRINT @THIS_PROGRAM_RELIES_ON_THE_FOLLOWING_ASSUPTIONS:)(PRINT(THV ASSL))(PRINC @;)))
51110 (COND((THV COMMENTLIST)(PRINT @COMMENT))
51112 (T(GO OU02)))
51113 (SETQ CLST(THV COMMENTLIST))
51115 OU4 (COND((NULL CLST)(PRINC @;)(GO OU02)))
51116 (TERPRI)
51120 (SETQ COMLST(CAR CLST))
51125 (THSETQ CLST(CDR CLST)T T)
51130 OU5 (COND((NULL COMLST)(GO OU4)))
51135 (PRINC(CAR COMLST))(PRINC @" ")
51140 (SETQ COMLST(CDR COMLST))
51145 (GO OU5)
51150 OU02 (SETQ INDENT NIL)
51200 (TSLPLAN GANS)
51250 (COND(STAT(TERPRI)
51300 (PRINT THME)(PRINC @__RULES_ENTERED)(PRINT THMS)(PRINC @__RULES_SUCCESSFUL)))
51400 (TERPRI)
51450 (COND((OR(NULL GSWI)(NULL GGEN))(RETURN T)))
51500 (SETQ GTYP1 GTYP) (SETQ GSTA1 GSTA) (SETQ GTAS1 GTAS)
51550 (PRINT @THIS_PLAN_HAS_ALSO_BEEN_GENERALIZED_AND_RESIDES_IN_THE)
51600 (PRINT @LIBRARY_IN_THE_FORM:)
51650 (TERPRI)
51690 (COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
51700 (PRINC GENAL)
51725 (TERPRI)
51750 OU3 (PRINC(CAAR GTYP1))(PRINC(CDAR GTYP1))
51800 (PRINC @;)
51850 (SETQ GTYP1(CDR GTYP1))
51900 (COND(GTYP1(GO OU3)))
51950 (PRINT @COMMENT)
52000 (PRINT @INPUT_CONDITIONS:)(TERPRI)
52050 (OUTCONDI GSTA1)
52100 (PRINT @OUTPUT_CONDITIONS:)(TERPRI)
52150 (OUTCONDI GTAS1)
52200 (PRINC @;)
52250 (TSLPLAN GSWI) (TERPRI) ))
52300 EXPR)
52350
52400
52450
52500 (DEFPROP OUTCONDI
52550 (LAMBDA(CC)
52600 (PROG(LCC)
52625 (COND((NULL CC)(PRINC @NONE)(RETURN T)))
52650 (SETQ LCC CC)
52700 OU00 (PRINC(CAAR LCC))
52750 (COND((EQ @R(CAR(LAST(CAR LCC))))
52800 (PRINC(REVERSE(CDR(REVERSE(CDAR LCC))))))
52850 (T(PRINC(CDAR LCC))))
52900 (SETQ LCC(CDR LCC))
52950 (COND(LCC(PRINC @∧)(GO OU00)))
53000 (RETURN T) ))
53050 EXPR)
53100
53150
53200
53250
53300
53350 (DEFPROP PROCJOIN
53400 (LAMBDA NIL
53450 (PROG(JC)
53500 (COND((NOT(SETQ JC(FINDCOND JOINCOND)))(RETURN T)))
53550 (SETQ SSW T)
53600 (SETQ JCFC(TESTJOIN JC))
53650 (SETQ SSW NIL)
53700 (COND((NULL JCFC)(RETURN T)))
53750 (RETURN NIL) ))
53800 EXPR)
53850
53900
53950 (DEFPROP FINDCOND
54000 (LAMBDA(JOC)
54050 (COND((NULL JOC)NIL)
54100 ((MEMBER PL(CAAR JOC))(CADAR JOC))
54150 (T(FINDCOND(CDR JOC)))))
54200 EXPR)
54250
54300 (DEFPROP TESTJOIN
54350 (LAMBDA(JC)
54400 (COND((NULL JC)NIL)
54450 ((THVAL @(THGOAL(THEV(CAR JC)))THALIST)
54500 (TESTJOIN(CDR JC)))
54550 (T(CAR JC))) )
54600 EXPR)
54650
54655 (DEFPROP STEPREF
54658 (LAMBDA(OPN ARGL GL)
54661 (PROG(ST)
54662 (COND((AND(THV WF)(THASVAL(THV FT)))(RETURN T)))
54664 (SETQ ST(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN))))))
54667 (SAVESTATE ST)
54670 (SETQ LIFOL(CONS(LIST(CONS OPN ARGL)GL ST)LIFOL))
54673 (THSETQ(THV ASSL)(CONS OPN(THV ASSL)))
54676 (RETURN T) ))
54679 EXPR)
54682
54685 (DEFPROP POPN
54688 (LAMBDA NIL
54692 (PROG(N)
54694 (SETQ N(LENGTH(THV ASSL)))
54697 PO2 (COND((ZEROP N)(RETURN T)))
54700 (SETQ N(SUB1 N))
54703 (SETQ LIFOL(CDR LIFOL))
54706 (GO PO2) ))
54709 EXPR)
54712
54715
54750 (DEFPROP SUBGOAL
54800 (LAMBDA (L)
54850 (PROG(JCFC PL GOL ST PREDLIST LGANS LCT INDENT STAT THME THMS GANS RES FILENAME COMPI GENAL LIBFIT
54900 PVARLIST GSWI GTDB GTAS GVL GCON GSTA GTYP GGEN IGTDB IGTAS FUNDEFLIST P1A P2A P3A P4A P5A)
54950 (CSYM NF00)
55000 SU0 (COND((EQ T(CAR L))(GO SU40)))
55050 (COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(SETQ FILENAME(CAR L))(GO SU10)))
55100 (COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
55150 (COMP L)
55200 SU10 (EVAL(LIST @DSKIN FILENAME))
55250 (COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
55300 (OUTC(OUTPUT DSK: INIT)T)
55350 (THDUMP)
55400 (OUTC NIL)
55410 (OUTC(OUTPUT PLIB DSK: PLIB)NIL)
55420 (OUTC NIL NIL)
55450 (SETQ ST @INIT)
55500 SU12 (PRINT @SUBMIT_GOAL*)
55550 (SETQ GOL(READ))
55560 (SETQ LIBFIT NIL)
55600 (SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
55610 (PRINT @DO_YOU_WANT_TO_TRY_USING_THE_PROGRAM_LIBRARY?)
55630 (COND((READ)(SETQ LIBFIT T)(DSKIN PLIB)))
55650 SU13 (PRINT @DO_YOU_HAVE_ANY_ADVICE?*)
55700 (COND((READ)(ADVICESYS)))
55750 SU15 (SETQ THME 0)(SETQ THMS 0)
55760 (THVSETQ(THV COMMENTLIST)NIL)
55800 (SETQ THSTEPT @(STEPT))
55850 (COND((AND(GET(CAR GOL)@FLUENT)(NOT(EQ @R(CAR(LAST GOL)))))(SETQ GOL(APPEND GOL(LIST @R)))))
55900 (SETQ RES(THVAL(LIST @THGOAL GOL(LIST @THTBF @THTRUE))THALIST))
55950 (SETQ THSTEPT NIL)
56000 (COND((NULL RES)(GO SU17)))
56050 (COND((PROCJOIN)(GO SU16)))
56100 (PRINT @THE_JOIN_CONDITION_)(PRINC JCFC)(PRINC @_FAILED!)
56150 (PRINT @HENCE_THE_PROCEDURE_IN_ITS_PRESENT_FORM_CANNOT_BE_USED)
56200 (PRINT @DO_YOU_WANT_TO_EXTEND_THE_PROCEDURE_)(PRINC PL)(PRINC @_TO_SATISFY_)(PRINC JCFC)(PRINC @*)
56250 (COND((READ)(SETQ GOL JCFC)(SETQ JCFC NIL)(GO SU13)))
56300 (GO SU20)
56350 SU16 (COND((THV PROCDATA)(CJOINCOND)))
56450 (COND((NULL GANS)(PRINT @GOAL_TRUE_IN_PRESENT_WORLD!)(TERPRI)(GO SU20)))
56500 (PRINT @DO_YOU_WANT_TO_OPTIMIZE_THE_PROGRAM?*)
56510 (COND((READ)(SETQ GANS(OPTIM GANS))))
56520 (GENERALIZE)
56530 (GO SU18)
56550 SU17 (PRINT @THE_GOAL_FAILED!__DO_YOU_WANT_TO_TRY_AGAIN_WITH_MORE_ADVICE?*)
56600 (COND((READ)(ADVICESYS)(GO SU15)))
56658 (GO SU20)
56700 SU18 (OUTANS)
56725 (PRINT PL)
56750 (EVAL(LIST @OUTC(LIST @OUTPUT @DSK: (COND((ATOM PL)PL)(T(CAR PL))))T))
56800 (OUTANS)
56850 (OUTC NIL)
56852 (COND((NULL(THV ASSL))(GO SU20)))
56855 (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
56858 (COND((NULL(READ))(POPN)(GO SU20)))
56861 SU19 (SETQ PL(CAR LIFOL))
56864 (SETQ LIFOL(CDR LIFOL))
56867 (GO SU25)
56900 SU20 (COND((NULL FIFOL)(GO SU28)))
56950 (PRINT @DO_YOU_WANT_TO_DO_CONTINGENCY_PLANNING?*)
57000 (COND((NULL(READ))(GO SU30)))
57050 (THSETQ(THV DBLITS)NIL T T)
57100 (THSETQ(THV ASSERTLITS)NIL T T)
57150 (PRINT @WHAT_IS_YOUR_PREFERENCE?__IF_NONE_TYPE_NIL*)
57200 SU22 (SETQ PL(READ))
57225 (PRINT @L57225)(PRINT PL)
57250 (COND((NULL PL)(SETQ PL(CAR FIFOL))(PRINT NIL)(PRINT PL)(SETQ FIFOL(CDR FIFOL)))
57300 ((SETQ PL(ASSOC PL FIFOL))(PRINT T)(PRINT PL)(SETQ FIFOL(DELAD1(CAR PL)FIFOL)))
57350 (T(PRINT @NO_SUCH_PROC___TRY_AGAIN*)(GO SU22)))
57400 SU25 (SETQ GOL(CADR PL))
57450 (COND((EQUAL(LAST GOL)@(R))(SETQ GOL(REVERSE(CDR(REVERSE GOL))))))
57500 (THFLUSH THASSERTION THERASING THCONSE)
57525 (PRINT @L57525)(PRINT PL)
57550 (SETQ ST(CADDR PL))
57575 (PRINT @L57575)(PRINT ST)
57600 (PRINT @TRYING___)(PRINC PL)
57650 (EVAL(LIST @DSKIN ST))
57700 (SETQ PL(CAR PL))
57750 (SETQ GANS NIL)
57800 (THVSETQ(THV PROCDATA)NIL)
57825 (THVSETQ(THV PASSUM)NIL)
57828 (THVSETQ(THV ASSL)NIL)
57850 (THVSET(CAR(THV ANS))NIL)
57900 (THSETQ(THV O1)@THUNASSIGNED)
57950 (SETQ LCT NIL)(SETQ LGANS NIL)
58000 (GO SU13)
58010 SU28 (COND((NULL(THV ASSL))(GO SU30)))
58013 (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
58016 (COND((NULL(READ))(GO SU30)))
58019 (GO SU19)
58050 SU30 (COND(JCFC(PRINT @INITIAL_STATE_REENTERED)(GO SU40)))
58100 (SETQ GANS NIL)
58150 (SETQ LCT NIL)(SETQ LGANS NIL)
58200 (PRINT @DO_YOU_WANT_TO_CONTINUE_FROM_THE_PRESENT_STATE_OF_THE_WORLD?)
58250 (COND((READ)(GO SU12)))
58300 SU40 (THFLUSH THASSERTION THERASING THCONSE)
58350 (THSETQ(THV DBLITS)NIL T T)
58400 (THSETQ(THV ASSERTLITS)NIL T T)
58450 (DSKIN INIT)
58500 (SETQ ST @INIT)
58550 (THVSETQ(THV PROCDATA)NIL)
58600 (THVSET(CAR(THV ANS))NIL)
58625 (THVSETQ(THV PASSUM)NIL)
58628 (THVSETQ(THV ASSL)NIL)
58650 (GO SU12)
58700 ))
58750 FEXPR)